T:Type, eq:EqDecider(T), es:ES, x:Id, e, e':E.
@loc(e')(x:T)  (e <loc e')  (((x after e) = (x when e')  T)  (lastchange(x;e') <loc e')) 

latex

Definitions	True, T, {T}, P  Q, ff, tt, if b then t else f fi , P  Q, P & Q, P  Q, , t  T, lastchange(x;e), P  Q, EqDecider(T), x:A. B(x), x:A. B(x), ee'.P(e), A c B, (e <loc e'), @i(x:T), Unit, ,
Lemmas	es-locl-iff, es-loc-pred, true wf, squash wf, es-le-loc, es-after-pred2, es-next, not-changed, es-when wf, es-vartype wf, es-after wf, last-change-property, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, changed wf, assert wf, iff wf, bool wf, event system wf, Id wf, es-E wf, es-loc wf, es-dtype wf, es-locl wf